a:Atom1, A:Type, v:A+Unit. AtomFree(Type;A)  isl(v)  outl(v):A>>a  v:A+Unit>>a 

latex

Definitions	Unit, Type, #$n, , s = t, t  T, AtomFree(T;x), P  Q, x:A. B(x), False, b, left+right, Atom$n, isl(x), outl(x), x:T>>a
Lemmas	inheres wf, outl wf, assert wf, isl wf, atom-free wf, inl-inherence, unit wf